#include <stddef.h>
#include <stdint.h>

void index_typedef(uint64_t *arr) {
    size_t foo3 = arr[25];
}
